Metaprogramming in Lean ログ

Syntax Quotations

code:memo

Lean.TSyntax `num

Lean.TSyntax

Lean.NumLit

Lean.numLitKind == Lean.TSyntax `num

code:memo

`($x)

`($$x)

`($x:kind) -- kind部分はSyntaxKind

syntax term,* : SomeStx

syntax term* : SomeStx

TSepArray c ","

declare_syntax_cat

code:memo

-- run the function given at the end for each element of the list

syntax "foreach " "term,* "" term : term

macro_rules

| (foreach [ $[$x:term],* ] $func:term) => (let f := $func; [ $f $x,* ])

#eval foreach 1,2,3,4 (Nat.add 2) -- 3, 4, 5, 6

-- let f := Nat.add = f 1, f 2, f 3, f 4

-- TSepArray `term "," →

code:lean

-- from Lean/Elab/Tactic/Basic.lean

TacticM = ReaderT Context $ StateRefT State TermElabM

let_expr

LeanのMVar

証明の途中における未解決の部分を表すメタ変数？